g:IMonoid, a:|g|. IsMonHom{<,+>,g}(n.n  a) 

latex

Up	groups 1
Definitions of Statement	|g|, *, e, IMonoid, IsMonHom{M1,M2}(f), <,+>
Definitions	t  T, t.2, t.1, x f y, e, *, FunThru2op(A;B;opa;opb;f), P & Q, <,+>, IsMonHom{M1,M2}(f), |g|, x:A. B(x), IMonoid
Lemmas	imon wf, grp car wf, mon nat op zero, nat wf, mon nat op add